/*
 * ClauseSet.cpp
 *
 * Copyright 2012 Fabian Wenzelmann
 *
 * This file is part of Recognition-Procedures-for-Boolean-Functions.
 *
 * Recognition-Procedures-for-Boolean-Functions is free software: you
 * can redistribute it and/or modify it under the terms of the
 * GNU General Public License as published by the Free Software Foundation,
 * either version 3 of the License, or (at your option) any later version.
 *
 * Recognition-Procedures-for-Boolean-Functions is distributed in the hope
 * that it will be useful, but WITHOUT ANY WARRANTY; without even the implied
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General
 * Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with Recognition-Procedures-for-Boolean-Functions.
 *
 * If not, see <http://www.gnu.org/licenses/>.
 */

#include "bfr/ClauseSet.hpp"

#include <string>
#include <iostream>
#include <sstream>

#include <boost/unordered_set.hpp>

#include "bfr/Clause.hpp"

namespace bfr {

ClauseSet::ClauseSet()
    : clauses(), maxID(0) { }

ClauseSet::ClauseSet(size_t initialSize)
    : clauses(2 * initialSize), maxID(0) { }

ClauseSet::~ClauseSet() {
    const_iterator it = begin();
    const_iterator e = end();
    while (it != e) {
        delete *it;
        it++;
    }
}

bool ClauseSet::add(const Clause *clause) {
    size_t count = clause->getMaxLiteralId();
    if (count > maxID)
        maxID = count;
    return clauses.insert(clause).second;
}

bool ClauseSet::addSecure(const Clause *clause) {
    if (!add(clause)) {
        delete clause;
        return false;
    }
    return true;
}

void ClauseSet::writeDIMACS(std::ostream &out) const {
    // TODO: use variableCount id method
    // first count the variables in the set
    size_t maxID = getMaxLiteralId();
    maxID++;

    out << "p dnf " << maxID << ' ' << size() << std::endl;

    const_iterator e = end();
    for (const_iterator it = begin(); it != e; it++) {
        const Clause *clause = *it;
        Clause::const_iterator ce = clause->end();
        bool first = true;
        for (Clause::const_iterator cit = clause->begin();
             cit != ce;
             cit++) {
            const Literal &l = *cit;
            if(first)
                first = false;
            else
                out << ' ';
            size_t id = l.getId() + 1;
            if(!l.getPolarity())
                out << '-';
            out << id;
        }
        // write "0"
        if(first)
            first = false;
        else
            out << ' ';
        out << "0";
        out << std::endl;
    }
}

std::string ClauseSet::asString() const {
    std::ostringstream stream;
    stream << *this;
    return stream.str();
}

bool ClauseSet::operator== (const ClauseSet &other) const {
        if (size() != other.size())
            return false;
        const_iterator it = begin();
        const_iterator e = end();
        while (it != e) {
            if (!other.contains(*it))
                return false;
            it++;
        }
        return true;
}

bool ClauseSet::operator!= (const ClauseSet &other) const {
    return !(*this == other);
}

} // namespace bfr
